Upcoming Event: PhD Dissertation Defense

Graph-Based Methods for Scalable and Verifiable Digital Twins

Luwen Huang, Ph.D. Candidate, Computer Science

Abstract

As the digital twin paradigm increasingly gains traction across diverse domains, its adoption remains limited by three core challenges: scalability, verifiability, and predictive capability. To date, most work on digital twins has focused on specific implementations or case studies, often centered on assembling existing technologies. What remains largely absent is a generalized mathematical formulation that abstracts away from specific technologies and that can be applied consistently across applications. This thesis develops a cohesive theoretical formulation that addresses these challenges through formalized knowledge representation, verifiable system dynamics, and explainable generative modeling. The formulation defines a two-layer, graph-based representation of a digital twin. At the foundational layer, an ontological knowledge graph captures system structure by organizing entities, relationships, and semantic rules governing their interactions. At the adaptive layer, a probabilistic graphical model governs the temporal evolution of these elements, providing a consistent mathematical basis for updates. Building on this foundation, the thesis develops a rigorous method for the formal verification of digital twins using the Temporal Logic of Actions. We leverage the adaptive layer to derive formal specifications of a digital twin under asynchronous, bidirectional communication, conditions characteristic of real-world operation. 

Finally, the work addresses the challenge of predictive modeling in data-restricted settings, where developing accurate models often requires data that are high-dimensional, costly, or restricted. We develop an explainable approach for generating longitudinal synthetic data that preserves key dependencies, supporting the development of predictive models for digital twins. These methods are demonstrated through two applications: an Educational Digital Twin modeling statewide student pathways for large-scale analysis, and an unmanned aerial vehicle digital twin illustrating formal verification in safety-critical systems. Together, these contributions establish a mathematical foundation for digital twins that generalizes across domains, supports formal verification, and strengthens predictive capability through explainable synthesis.

Biography